n:, T:Type, R:(TTprop{i:l}). rel_exp(T; R; n)  TTprop{i:l} 

latex

Definitions	False, A, A  B, ge(i; j), P  Q, x f y, P  Q, x:A. B(x), t  T, prop{i:l}, x:A. B(x),
Lemmas	ge wf, nat properties, not wf, bnot wf, assert wf, bool wf, eq int wf